0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 284 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 331 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 PiDPToQDPProof (⇒, 12 ms)
↳23 QDP
↳24 QDPSizeChangeProof (⇔, 0 ms)
↳25 YES
INSERTA_IN_GGA(s(X1), tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U6_GGA(X1, X2, X3, X4, pB_in_gga(X1, X2, X4))
INSERTA_IN_GGA(s(X1), tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → PB_IN_GGA(X1, X2, X4)
PB_IN_GGA(X1, X2, X3) → U2_GGA(X1, X2, X3, lessC_in_g(X1))
PB_IN_GGA(X1, X2, X3) → LESSC_IN_G(X1)
LESSC_IN_G(s(X1)) → U1_G(X1, lessC_in_g(X1))
LESSC_IN_G(s(X1)) → LESSC_IN_G(X1)
PB_IN_GGA(X1, X2, X3) → U3_GGA(X1, X2, X3, lesscC_in_g(X1))
U3_GGA(X1, X2, X3, lesscC_out_g(X1)) → U4_GGA(X1, X2, X3, insertA_in_gga(s(X1), X2, X3))
U3_GGA(X1, X2, X3, lesscC_out_g(X1)) → INSERTA_IN_GGA(s(X1), X2, X3)
INSERTA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → U7_GGA(X1, X2, X3, X4, lessC_in_g(X1))
INSERTA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → LESSC_IN_G(X1)
INSERTA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → U8_GGA(X1, X2, X3, X4, lesscC_in_g(X1))
U8_GGA(X1, X2, X3, X4, lesscC_out_g(X1)) → U9_GGA(X1, X2, X3, X4, insertA_in_gga(X1, X3, X4))
U8_GGA(X1, X2, X3, X4, lesscC_out_g(X1)) → INSERTA_IN_GGA(X1, X3, X4)
INSERTA_IN_GGA(s(X1), tree(s(X1), X2, X3), tree(s(X1), X2, X4)) → U10_GGA(X1, X2, X3, X4, pB_in_gga(X1, X3, X4))
INSERTA_IN_GGA(s(X1), tree(s(X1), X2, X3), tree(s(X1), X2, X4)) → PB_IN_GGA(X1, X3, X4)
INSERTA_IN_GGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U11_GGA(X1, X2, X3, X4, insertA_in_gga(0, X2, X4))
INSERTA_IN_GGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → INSERTA_IN_GGA(0, X2, X4)
INSERTA_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), tree(s(s(s(s(s(s(s(s(X2)))))))), X3, X4), tree(s(s(s(s(s(s(s(s(X2)))))))), X5, X4)) → U12_GGA(X1, X2, X3, X4, X5, lessE_in_gg(X1, X2))
INSERTA_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), tree(s(s(s(s(s(s(s(s(X2)))))))), X3, X4), tree(s(s(s(s(s(s(s(s(X2)))))))), X5, X4)) → LESSE_IN_GG(X1, X2)
LESSE_IN_GG(s(X1), s(X2)) → U5_GG(X1, X2, lessE_in_gg(X1, X2))
LESSE_IN_GG(s(X1), s(X2)) → LESSE_IN_GG(X1, X2)
INSERTA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U13_GGA(X1, X2, X3, X4, X5, lesscD_in_gg(X1, X2))
U13_GGA(X1, X2, X3, X4, X5, lesscD_out_gg(X1, X2)) → U14_GGA(X1, X2, X3, X4, X5, insertA_in_gga(s(X1), X3, X5))
U13_GGA(X1, X2, X3, X4, X5, lesscD_out_gg(X1, X2)) → INSERTA_IN_GGA(s(X1), X3, X5)
INSERTA_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U15_GGA(X1, X2, X3, X4, X5, lessE_in_gg(X2, X1))
INSERTA_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → LESSE_IN_GG(X2, X1)
INSERTA_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U16_GGA(X1, X2, X3, X4, X5, lesscE_in_gg(X2, X1))
U16_GGA(X1, X2, X3, X4, X5, lesscE_out_gg(X2, X1)) → U17_GGA(X1, X2, X3, X4, X5, insertA_in_gga(X1, X4, X5))
U16_GGA(X1, X2, X3, X4, X5, lesscE_out_gg(X2, X1)) → INSERTA_IN_GGA(X1, X4, X5)
INSERTA_IN_GGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U18_GGA(X1, X2, X3, X4, insertA_in_gga(s(X1), X3, X4))
INSERTA_IN_GGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → INSERTA_IN_GGA(s(X1), X3, X4)
INSERTA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U19_GGA(X1, X2, X3, X4, X5, lessE_in_gg(X2, X1))
INSERTA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → LESSE_IN_GG(X2, X1)
INSERTA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U20_GGA(X1, X2, X3, X4, X5, lesscE_in_gg(X2, X1))
U20_GGA(X1, X2, X3, X4, X5, lesscE_out_gg(X2, X1)) → U21_GGA(X1, X2, X3, X4, X5, insertA_in_gga(s(X1), X4, X5))
U20_GGA(X1, X2, X3, X4, X5, lesscE_out_gg(X2, X1)) → INSERTA_IN_GGA(s(X1), X4, X5)
lesscC_in_g(s(X1)) → U35_g(X1, lesscC_in_g(X1))
U35_g(X1, lesscC_out_g(X1)) → lesscC_out_g(s(X1))
lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(0), s(s(X1))) → lesscD_out_gg(s(0), s(s(X1)))
lesscD_in_gg(s(s(0)), s(s(s(X1)))) → lesscD_out_gg(s(s(0)), s(s(s(X1))))
lesscD_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscD_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscD_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscD_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscD_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscD_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscD_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscD_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscD_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U39_gg(X1, X2, lesscE_in_gg(X1, X2))
lesscE_in_gg(0, s(X1)) → lesscE_out_gg(0, s(X1))
lesscE_in_gg(s(X1), s(X2)) → U38_gg(X1, X2, lesscE_in_gg(X1, X2))
U38_gg(X1, X2, lesscE_out_gg(X1, X2)) → lesscE_out_gg(s(X1), s(X2))
U39_gg(X1, X2, lesscE_out_gg(X1, X2)) → lesscD_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
INSERTA_IN_GGA(s(X1), tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U6_GGA(X1, X2, X3, X4, pB_in_gga(X1, X2, X4))
INSERTA_IN_GGA(s(X1), tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → PB_IN_GGA(X1, X2, X4)
PB_IN_GGA(X1, X2, X3) → U2_GGA(X1, X2, X3, lessC_in_g(X1))
PB_IN_GGA(X1, X2, X3) → LESSC_IN_G(X1)
LESSC_IN_G(s(X1)) → U1_G(X1, lessC_in_g(X1))
LESSC_IN_G(s(X1)) → LESSC_IN_G(X1)
PB_IN_GGA(X1, X2, X3) → U3_GGA(X1, X2, X3, lesscC_in_g(X1))
U3_GGA(X1, X2, X3, lesscC_out_g(X1)) → U4_GGA(X1, X2, X3, insertA_in_gga(s(X1), X2, X3))
U3_GGA(X1, X2, X3, lesscC_out_g(X1)) → INSERTA_IN_GGA(s(X1), X2, X3)
INSERTA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → U7_GGA(X1, X2, X3, X4, lessC_in_g(X1))
INSERTA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → LESSC_IN_G(X1)
INSERTA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → U8_GGA(X1, X2, X3, X4, lesscC_in_g(X1))
U8_GGA(X1, X2, X3, X4, lesscC_out_g(X1)) → U9_GGA(X1, X2, X3, X4, insertA_in_gga(X1, X3, X4))
U8_GGA(X1, X2, X3, X4, lesscC_out_g(X1)) → INSERTA_IN_GGA(X1, X3, X4)
INSERTA_IN_GGA(s(X1), tree(s(X1), X2, X3), tree(s(X1), X2, X4)) → U10_GGA(X1, X2, X3, X4, pB_in_gga(X1, X3, X4))
INSERTA_IN_GGA(s(X1), tree(s(X1), X2, X3), tree(s(X1), X2, X4)) → PB_IN_GGA(X1, X3, X4)
INSERTA_IN_GGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U11_GGA(X1, X2, X3, X4, insertA_in_gga(0, X2, X4))
INSERTA_IN_GGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → INSERTA_IN_GGA(0, X2, X4)
INSERTA_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), tree(s(s(s(s(s(s(s(s(X2)))))))), X3, X4), tree(s(s(s(s(s(s(s(s(X2)))))))), X5, X4)) → U12_GGA(X1, X2, X3, X4, X5, lessE_in_gg(X1, X2))
INSERTA_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), tree(s(s(s(s(s(s(s(s(X2)))))))), X3, X4), tree(s(s(s(s(s(s(s(s(X2)))))))), X5, X4)) → LESSE_IN_GG(X1, X2)
LESSE_IN_GG(s(X1), s(X2)) → U5_GG(X1, X2, lessE_in_gg(X1, X2))
LESSE_IN_GG(s(X1), s(X2)) → LESSE_IN_GG(X1, X2)
INSERTA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U13_GGA(X1, X2, X3, X4, X5, lesscD_in_gg(X1, X2))
U13_GGA(X1, X2, X3, X4, X5, lesscD_out_gg(X1, X2)) → U14_GGA(X1, X2, X3, X4, X5, insertA_in_gga(s(X1), X3, X5))
U13_GGA(X1, X2, X3, X4, X5, lesscD_out_gg(X1, X2)) → INSERTA_IN_GGA(s(X1), X3, X5)
INSERTA_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U15_GGA(X1, X2, X3, X4, X5, lessE_in_gg(X2, X1))
INSERTA_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → LESSE_IN_GG(X2, X1)
INSERTA_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U16_GGA(X1, X2, X3, X4, X5, lesscE_in_gg(X2, X1))
U16_GGA(X1, X2, X3, X4, X5, lesscE_out_gg(X2, X1)) → U17_GGA(X1, X2, X3, X4, X5, insertA_in_gga(X1, X4, X5))
U16_GGA(X1, X2, X3, X4, X5, lesscE_out_gg(X2, X1)) → INSERTA_IN_GGA(X1, X4, X5)
INSERTA_IN_GGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U18_GGA(X1, X2, X3, X4, insertA_in_gga(s(X1), X3, X4))
INSERTA_IN_GGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → INSERTA_IN_GGA(s(X1), X3, X4)
INSERTA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U19_GGA(X1, X2, X3, X4, X5, lessE_in_gg(X2, X1))
INSERTA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → LESSE_IN_GG(X2, X1)
INSERTA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U20_GGA(X1, X2, X3, X4, X5, lesscE_in_gg(X2, X1))
U20_GGA(X1, X2, X3, X4, X5, lesscE_out_gg(X2, X1)) → U21_GGA(X1, X2, X3, X4, X5, insertA_in_gga(s(X1), X4, X5))
U20_GGA(X1, X2, X3, X4, X5, lesscE_out_gg(X2, X1)) → INSERTA_IN_GGA(s(X1), X4, X5)
lesscC_in_g(s(X1)) → U35_g(X1, lesscC_in_g(X1))
U35_g(X1, lesscC_out_g(X1)) → lesscC_out_g(s(X1))
lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(0), s(s(X1))) → lesscD_out_gg(s(0), s(s(X1)))
lesscD_in_gg(s(s(0)), s(s(s(X1)))) → lesscD_out_gg(s(s(0)), s(s(s(X1))))
lesscD_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscD_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscD_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscD_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscD_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscD_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscD_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscD_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscD_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U39_gg(X1, X2, lesscE_in_gg(X1, X2))
lesscE_in_gg(0, s(X1)) → lesscE_out_gg(0, s(X1))
lesscE_in_gg(s(X1), s(X2)) → U38_gg(X1, X2, lesscE_in_gg(X1, X2))
U38_gg(X1, X2, lesscE_out_gg(X1, X2)) → lesscE_out_gg(s(X1), s(X2))
U39_gg(X1, X2, lesscE_out_gg(X1, X2)) → lesscD_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))
LESSE_IN_GG(s(X1), s(X2)) → LESSE_IN_GG(X1, X2)
lesscC_in_g(s(X1)) → U35_g(X1, lesscC_in_g(X1))
U35_g(X1, lesscC_out_g(X1)) → lesscC_out_g(s(X1))
lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(0), s(s(X1))) → lesscD_out_gg(s(0), s(s(X1)))
lesscD_in_gg(s(s(0)), s(s(s(X1)))) → lesscD_out_gg(s(s(0)), s(s(s(X1))))
lesscD_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscD_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscD_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscD_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscD_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscD_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscD_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscD_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscD_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U39_gg(X1, X2, lesscE_in_gg(X1, X2))
lesscE_in_gg(0, s(X1)) → lesscE_out_gg(0, s(X1))
lesscE_in_gg(s(X1), s(X2)) → U38_gg(X1, X2, lesscE_in_gg(X1, X2))
U38_gg(X1, X2, lesscE_out_gg(X1, X2)) → lesscE_out_gg(s(X1), s(X2))
U39_gg(X1, X2, lesscE_out_gg(X1, X2)) → lesscD_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))
LESSE_IN_GG(s(X1), s(X2)) → LESSE_IN_GG(X1, X2)
LESSE_IN_GG(s(X1), s(X2)) → LESSE_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
LESSC_IN_G(s(X1)) → LESSC_IN_G(X1)
lesscC_in_g(s(X1)) → U35_g(X1, lesscC_in_g(X1))
U35_g(X1, lesscC_out_g(X1)) → lesscC_out_g(s(X1))
lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(0), s(s(X1))) → lesscD_out_gg(s(0), s(s(X1)))
lesscD_in_gg(s(s(0)), s(s(s(X1)))) → lesscD_out_gg(s(s(0)), s(s(s(X1))))
lesscD_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscD_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscD_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscD_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscD_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscD_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscD_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscD_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscD_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U39_gg(X1, X2, lesscE_in_gg(X1, X2))
lesscE_in_gg(0, s(X1)) → lesscE_out_gg(0, s(X1))
lesscE_in_gg(s(X1), s(X2)) → U38_gg(X1, X2, lesscE_in_gg(X1, X2))
U38_gg(X1, X2, lesscE_out_gg(X1, X2)) → lesscE_out_gg(s(X1), s(X2))
U39_gg(X1, X2, lesscE_out_gg(X1, X2)) → lesscD_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))
LESSC_IN_G(s(X1)) → LESSC_IN_G(X1)
LESSC_IN_G(s(X1)) → LESSC_IN_G(X1)
From the DPs we obtained the following set of size-change graphs:
INSERTA_IN_GGA(s(X1), tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → PB_IN_GGA(X1, X2, X4)
PB_IN_GGA(X1, X2, X3) → U3_GGA(X1, X2, X3, lesscC_in_g(X1))
U3_GGA(X1, X2, X3, lesscC_out_g(X1)) → INSERTA_IN_GGA(s(X1), X2, X3)
INSERTA_IN_GGA(X1, tree(X1, X2, X3), tree(X1, X2, X4)) → U8_GGA(X1, X2, X3, X4, lesscC_in_g(X1))
U8_GGA(X1, X2, X3, X4, lesscC_out_g(X1)) → INSERTA_IN_GGA(X1, X3, X4)
INSERTA_IN_GGA(s(X1), tree(s(X1), X2, X3), tree(s(X1), X2, X4)) → PB_IN_GGA(X1, X3, X4)
INSERTA_IN_GGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → INSERTA_IN_GGA(0, X2, X4)
INSERTA_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U16_GGA(X1, X2, X3, X4, X5, lesscE_in_gg(X2, X1))
U16_GGA(X1, X2, X3, X4, X5, lesscE_out_gg(X2, X1)) → INSERTA_IN_GGA(X1, X4, X5)
INSERTA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U13_GGA(X1, X2, X3, X4, X5, lesscD_in_gg(X1, X2))
U13_GGA(X1, X2, X3, X4, X5, lesscD_out_gg(X1, X2)) → INSERTA_IN_GGA(s(X1), X3, X5)
INSERTA_IN_GGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → INSERTA_IN_GGA(s(X1), X3, X4)
INSERTA_IN_GGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U20_GGA(X1, X2, X3, X4, X5, lesscE_in_gg(X2, X1))
U20_GGA(X1, X2, X3, X4, X5, lesscE_out_gg(X2, X1)) → INSERTA_IN_GGA(s(X1), X4, X5)
lesscC_in_g(s(X1)) → U35_g(X1, lesscC_in_g(X1))
U35_g(X1, lesscC_out_g(X1)) → lesscC_out_g(s(X1))
lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(0), s(s(X1))) → lesscD_out_gg(s(0), s(s(X1)))
lesscD_in_gg(s(s(0)), s(s(s(X1)))) → lesscD_out_gg(s(s(0)), s(s(s(X1))))
lesscD_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscD_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscD_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscD_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscD_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscD_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscD_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscD_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscD_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U39_gg(X1, X2, lesscE_in_gg(X1, X2))
lesscE_in_gg(0, s(X1)) → lesscE_out_gg(0, s(X1))
lesscE_in_gg(s(X1), s(X2)) → U38_gg(X1, X2, lesscE_in_gg(X1, X2))
U38_gg(X1, X2, lesscE_out_gg(X1, X2)) → lesscE_out_gg(s(X1), s(X2))
U39_gg(X1, X2, lesscE_out_gg(X1, X2)) → lesscD_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))
INSERTA_IN_GGA(s(X1), tree(s(X1), X2, X3)) → PB_IN_GGA(X1, X2)
PB_IN_GGA(X1, X2) → U3_GGA(X1, X2, lesscC_in_g(X1))
U3_GGA(X1, X2, lesscC_out_g(X1)) → INSERTA_IN_GGA(s(X1), X2)
INSERTA_IN_GGA(X1, tree(X1, X2, X3)) → U8_GGA(X1, X2, X3, lesscC_in_g(X1))
U8_GGA(X1, X2, X3, lesscC_out_g(X1)) → INSERTA_IN_GGA(X1, X3)
INSERTA_IN_GGA(s(X1), tree(s(X1), X2, X3)) → PB_IN_GGA(X1, X3)
INSERTA_IN_GGA(0, tree(s(X1), X2, X3)) → INSERTA_IN_GGA(0, X2)
INSERTA_IN_GGA(X1, tree(X2, X3, X4)) → U16_GGA(X1, X2, X3, X4, lesscE_in_gg(X2, X1))
U16_GGA(X1, X2, X3, X4, lesscE_out_gg(X2, X1)) → INSERTA_IN_GGA(X1, X4)
INSERTA_IN_GGA(s(X1), tree(s(X2), X3, X4)) → U13_GGA(X1, X2, X3, X4, lesscD_in_gg(X1, X2))
U13_GGA(X1, X2, X3, X4, lesscD_out_gg(X1, X2)) → INSERTA_IN_GGA(s(X1), X3)
INSERTA_IN_GGA(s(X1), tree(0, X2, X3)) → INSERTA_IN_GGA(s(X1), X3)
INSERTA_IN_GGA(s(X1), tree(s(X2), X3, X4)) → U20_GGA(X1, X2, X3, X4, lesscE_in_gg(X2, X1))
U20_GGA(X1, X2, X3, X4, lesscE_out_gg(X2, X1)) → INSERTA_IN_GGA(s(X1), X4)
lesscC_in_g(s(X1)) → U35_g(X1, lesscC_in_g(X1))
U35_g(X1, lesscC_out_g(X1)) → lesscC_out_g(s(X1))
lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(0), s(s(X1))) → lesscD_out_gg(s(0), s(s(X1)))
lesscD_in_gg(s(s(0)), s(s(s(X1)))) → lesscD_out_gg(s(s(0)), s(s(s(X1))))
lesscD_in_gg(s(s(s(0))), s(s(s(s(X1))))) → lesscD_out_gg(s(s(s(0))), s(s(s(s(X1)))))
lesscD_in_gg(s(s(s(s(0)))), s(s(s(s(s(X1)))))) → lesscD_out_gg(s(s(s(s(0)))), s(s(s(s(s(X1))))))
lesscD_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1))))))) → lesscD_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))))
lesscD_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1)))))))) → lesscD_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))))
lesscD_in_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2)))))))) → U39_gg(X1, X2, lesscE_in_gg(X1, X2))
lesscE_in_gg(0, s(X1)) → lesscE_out_gg(0, s(X1))
lesscE_in_gg(s(X1), s(X2)) → U38_gg(X1, X2, lesscE_in_gg(X1, X2))
U38_gg(X1, X2, lesscE_out_gg(X1, X2)) → lesscE_out_gg(s(X1), s(X2))
U39_gg(X1, X2, lesscE_out_gg(X1, X2)) → lesscD_out_gg(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(X2))))))))
lesscC_in_g(x0)
U35_g(x0, x1)
lesscD_in_gg(x0, x1)
lesscE_in_gg(x0, x1)
U38_gg(x0, x1, x2)
U39_gg(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs: